1  /-
  2  Copyright (c) 2019 Johannes Hölzl, Zhouhang Zhou. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Zhouhang Zhou
  5  -/
  6  
  7  import measure_theory.integration
src         └────────────────────────┘
  8  
  9  /-!
 10  
 11  # Almost everywhere equal functions
 12  
 13  Two measurable functions are treated as identical if they are almost everywhere equal. We form the
 14  set of equivalence classes under the relation of being almost everywhere equal, which is sometimes
 15  known as the `L⁰` space.
 16  
 17  See `l1_space.lean` for `L¹` space.
 18  
 19  
 20  ## Notation
 21  
 22  * `α →ₘ β` is the type of `L⁰` space, where `α` is a measure space and `β` is a measurable space.
 23    `f : α →ₘ β` is a "function" in `L⁰`. In comments, `[f]` is also used to denote an `L⁰` function.
 24  
 25    `ₘ` can be typed as `\_m`. Sometimes it is shown as a box if font is missing.
 26  
 27  
 28  ## Main statements
 29  
 30  * The linear structure of `L⁰` :
 31      Addition and scalar multiplication are defined on `L⁰` in the natural way, i.e.,
 32      `[f] + [g] := [f + g]`, `c • [f] := [c • f]`. So defined, `α →ₘ β` inherits the linear structure
 33      of `β`. For example, if `β` is a module, then `α →ₘ β` is a module over the same ring.
 34  
 35      See `mk_add_mk`,  `neg_mk`,     `mk_sub_mk`,  `smul_mk`,
 36          `add_to_fun`, `neg_to_fun`, `sub_to_fun`, `smul_to_fun`
 37  
 38  * The order structure of `L⁰` :
 39      `≤` can be defined in a similar way: `[f] ≤ [g]` if `f a ≤ g a` for almost all `a` in domain.
 40      And `α →ₘ β` inherits the preorder and partial order of `β`.
 41  
 42      TODO: Define `sup` and `inf` on `L⁰` so that it forms a lattice. It seems that `β` must be a
 43      linear order, since otherwise `f ⊔ g` may not be a measurable function.
 44  
 45  * Emetric on `L⁰` :
 46      If `β` is an `emetric_space`, then `L⁰` can be made into an `emetric_space`, where
 47      `edist [f] [g]` is defined to be `∫⁻ a, edist (f a) (g a)`.
 48  
 49      The integral used here is `lintegral : (α → ennreal) → ennreal`, which is defined in the file
 50      `integration.lean`.
 51  
 52      See `edist_mk_mk` and `edist_to_fun`.
 53  
 54  
 55  ## Implementation notes
 56  
 57  * `f.to_fun`     : To find a representative of `f : α →ₘ β`, use `f.to_fun`.
 58                   For each operation `op` in `L⁰`, there is a lemma called `op_to_fun`, characterizing,
 59                   say, `(f op g).to_fun`.
 60  * `ae_eq_fun.mk` : To constructs an `L⁰` function `α →ₘ β` from a measurable function `f : α → β`,
 61                   use `ae_eq_fun.mk`
 62  * `comp`         : Use `comp g f` to get `[g ∘ f]` from `g : β → γ` and `[f] : α →ₘ γ`
 63  * `comp₂`        : Use `comp₂ g f₁ f₂ to get `[λa, g (f₁ a) (f₂ a)]`.
 64                   For example, `[f + g]` is `comp₂ (+)`
 65  
 66  
 67  ## Tags
 68  
 69  function space, almost everywhere equal, `L⁰`, ae_eq_fun
 70  
 71  -/
 72  
 73  noncomputable theory
 74  open_locale classical
 75  
 76  namespace measure_theory
 77  open set lattice filter topological_space
 78  
 79  universes u v
 80  variables {α : Type u} {β : Type v} [measure_space α]
id                                        └───────────┘
src                                       └───────────┘
typ                                       └───────────┘
doc                                       └───────────┘
 81  
 82  section measurable_space
 83  variables [measurable_space β]
id              └──────────────┘
src             └──────────────┘
typ             └──────────────┘
 84  
 85  variables (α β)
 86  
 87  /-- The equivalence relation of being almost everywhere equal -/
 88  instance ae_eq_fun.setoid : setoid { f : α → β // measurable f } :=
id                               └────┘            └────────┘ 
src                              └────┘               └────────┘
typ                              └────┘            └────────┘ 
doc                                                    └────────┘
 89  ⟨ λf g, ∀ₘ a, f.1 a = g.1 a,
id         └┘        
src          └┘          
typ        └┘        
doc          └┘  
 90    assume ⟨f, hf⟩, by filter_upwards [] assume a, rfl,
id                                                   └─┘
src                       └────────────────┘      └──┘└─┘
typ                      └────────────────┘      └──┘└─┘
doc                       └────────────────┘      └──┘
txt                       └────────────────┘      └──┘
par                       └────────────────┘      └──┘
pid                                     └─┘      └──┘
st                       └──────────────────────────────┘
 91    assume ⟨f, hf⟩ ⟨g, hg⟩ hfg, by filter_upwards [hfg] assume a, eq.symm,
id                          └─┘                                    └─────┘
src                                   └──────────────┘   └┘      └──┘└─────┘
typ                         └─┘     └──────────────┘   └┘      └──┘└─────┘
doc                                   └──────────────┘   └┘      └──┘
txt                                   └──────────────┘   └┘      └──┘
par                                   └──────────────┘   └┘      └──┘
pid                                                 └┘         └──┘
st                                   └─────────────────────────────────────┘
 92    assume ⟨f, hf⟩ ⟨g, hg⟩ ⟨h, hh⟩ hfg hgh, by filter_upwards [hfg, hgh] assume a, eq.trans ⟩
id                                 └─┘ └─┘                                         └──────┘
src                                               └──────────────┘   └┘   └┘      └──┘└──────┘
typ                                └─┘ └─┘     └──────────────┘   └┘   └┘      └──┘└──────┘
doc                                               └──────────────┘   └┘   └┘      └──┘        
txt                                               └──────────────┘   └┘   └┘      └──┘        
par                                               └──────────────┘   └┘   └┘      └──┘        
pid                                                             └┘   └┘         └──┘        
st                                               └────────────────────────────────────────────┘
 93  
 94  /-- The space of equivalence classes of measurable functions, where two measurable functions are
 95      equivalent if they agree almost everywhere, i.e., they differ on a set of measure `0`.  -/
 96  def ae_eq_fun : Type (max u v) := quotient (ae_eq_fun.setoid α β)
id                                     └──────┘  └──────────────┘  
src                                    └──────┘  └──────────────┘
typ                                    └──────┘  └──────────────┘  
doc                                              └──────────────┘
 97  
 98  variables {α β}
 99  
100  infixr ` →ₘ `:25 := ae_eq_fun
id                       └───────┘
src                      └───────┘
typ                      └───────┘
doc                      └───────┘
101  
102  end measurable_space
103  
104  namespace ae_eq_fun
105  variables [measurable_space β]
id              └──────────────┘
src             └──────────────┘
typ             └──────────────┘
106  
107  /-- Construct the equivalence class `[f]` of a measurable function `f`, based on the equivalence
108      relation of being almost everywhere equal. -/
109  def mk (f : α → β) (hf : measurable f) : α →ₘ β := quotient.mk ⟨f, hf⟩
id                          └────────┘      └┘     └─────────┘    └┘
src                           └────────┘        └┘      └─────────┘
typ                         └────────┘      └┘     └─────────┘    └┘
doc                           └────────┘        └┘
110  
111  /-- A representative of an `ae_eq_fun` [f] -/
112  protected def to_fun (f : α →ₘ β) : α → β := @quotient.out _ (ae_eq_fun.setoid α β) f
id                              └┘             └──────────┘    └──────────────┘    
src                              └┘                └──────────┘    └──────────────┘
typ                             └┘             └──────────┘    └──────────────┘    
doc                              └┘                └──────────┘    └──────────────┘
113  
114  protected lemma measurable (f : α →ₘ β) : measurable f.to_fun :=
id                                    └┘     └────────┘ └─────┘
src                                    └┘      └────────┘  └─────┘
typ                                   └┘     └────────┘ └─────┘
doc                                    └┘      └────────┘  └─────┘
115  (@quotient.out _ (ae_eq_fun.setoid α β) f).2
id     └──────────┘    └──────────────┘     
src    └──────────┘    └──────────────┘        
typ    └──────────┘    └──────────────┘     
doc    └──────────┘    └──────────────┘
116  
117  instance : has_coe (α →ₘ β) (α → β) := ⟨λf, f.to_fun⟩
id              └─────┘   └┘                └─────┘
src             └─────┘    └┘                     └─────┘
typ             └─────┘   └┘                └─────┘
doc                        └┘                     └─────┘
118  
119  @[simp] lemma quot_mk_eq_mk (f : {f : α → β // measurable f}) : quot.mk setoid.r f = mk f.1 f.2 :=
id                                              └────────┘      └─────┘ └──────┘   └┘   
src                                                └────────┘               └──────┘    └┘     
typ                                             └────────┘      └─────┘ └──────┘   └┘   
doc    └──┘                                         └────────┘                            └┘
120  by cases f; refl
id            
src     └────┘   └────
typ     └────┘  └────
doc     └────┘   └────
txt     └────┘   └────
par     └────┘   └────
pid                 
st     └──────────────
121  
src  
typ  
doc  
txt  
par  
pid  
st   
122  @[simp] lemma mk_eq_mk (f g : α → β) (hf hg) :
id                                    
typ                                   
doc    └──┘
123    mk f hf = mk g hg ↔ (∀ₘ a, f a = g a) :=
id     └┘  └┘  └┘  └┘   └┘      
src    └┘       └┘        └┘       
typ    └┘  └┘  └┘  └┘   └┘      
doc    └┘        └┘         └┘  
124  ⟨quotient.exact, assume h, quotient.sound h⟩
id    └────────────┘           └────────────┘ 
src   └────────────┘            └────────────┘
typ   └────────────┘           └────────────┘ 
125  
126  @[ext] lemma ext (f g : α →ₘ β) (f' g' : α → β) (hf' hg') (hf : mk f' hf' = f)
id                            └┘                                 └┘ └┘ └─┘  
src                            └┘                                    └┘        
typ                           └┘                                 └┘ └┘ └─┘  
doc    └─┘                     └┘                                    └┘
127    (hg : mk g' hg' = g) (h : ∀ₘ a, f' a = g' a) : f = g :=
id           └┘ └┘ └─┘         └┘  └┘   └┘       
src          └┘                 └┘                   
typ          └┘ └┘ └─┘         └┘  └┘   └┘       
doc          └┘                  └┘  
128  by { rw [← hf, ← hg], rw mk_eq_mk, assumption }
id              └┘    └┘      └──────┘
src       └────┘  └──┘    └─┘└──────┘  └─────────┘
typ       └────┘└┘└──┘└┘  └─┘└──────┘  └─────────┘
doc       └────┘  └──┘    └─┘          └─────────┘
txt       └────┘  └──┘    └─┘          └─────────┘
par       └────┘  └──┘    └─┘          └─────────┘
pid         └──┘  └──┘                          
st     └─────────┘└────┘└────────────┘└───────────┘└┘
129  
130  lemma self_eq_mk (f : α →ₘ β) : f = mk (f.to_fun) f.measurable :=
id                          └┘       └┘  └─────┘  └─────────┘
src                          └┘         └┘   └─────┘   └─────────┘
typ                         └┘       └┘  └─────┘  └─────────┘
doc                          └┘          └┘   └─────┘
131  by simp [mk, ae_eq_fun.to_fun]
id            └┘  └──────────────┘
src     └────┘└┘└┘└──────────────┘└─
typ     └────┘└┘└┘└──────────────┘└─
doc     └────┘└┘└┘└──────────────┘└─
txt     └────┘  └┘                └─
par     └────┘  └┘                └─
pid           └┘                
st     └────────────────────────────
132  
src  
typ  
doc  
txt  
par  
pid  
st   
133  lemma all_ae_mk_to_fun (f : α → β) (hf) : ∀ₘ a, (mk f hf).to_fun a = f a :=
id                                           └┘   └┘  └┘ └────┘     
src                                            └┘    └┘      └────┘    
typ                                          └┘   └┘  └┘ └────┘     
doc                                            └┘    └┘      └────┘
134  by rw [← mk_eq_mk _ f _ hf, ← self_eq_mk (mk f hf)]
id            └──────┘      └┘    └────────┘  └┘  └┘
src     └────┘└──────┘└─┘ └─┘  └──┘└────────┘ └┘   └──
typ     └────┘└──────┘└─┘└─┘└┘└──┘└────────┘ └┘└┘└──
doc     └────┘        └─┘ └─┘  └──┘           └┘   └──
txt     └────┘        └─┘ └─┘  └──┘                └──
par     └────┘        └─┘ └─┘  └──┘                └──
pid       └──┘        └─┘ └─┘  └──┘                └┘
st     └──────────────────────┘└──────────────────────┘
135  
src  
typ  
doc  
txt  
par  
pid  
st   
136  /-- Given a measurable function `g : β → γ`, and an almost everywhere equal function `[f] : α →ₘ β`,
137      return the equivalence class of `g ∘ f`, i.e., the almost everywhere equal function
138      `[g ∘ f] : α →ₘ γ`. -/
139  def comp {γ : Type*} [measurable_space γ] (g : β → γ) (hg : measurable g) (f : α →ₘ β) : α →ₘ γ :=
id                         └──────────────┘                   └────────┘         └┘      └┘ 
src                        └──────────────┘                      └────────┘           └┘        └┘
typ                        └──────────────┘                   └────────┘         └┘      └┘ 
doc                                                              └────────┘           └┘        └┘
140  quotient.lift_on f (λf, mk (g ∘ f.1)  (measurable.comp hg f.2)) $ assume f₁ f₂ eq,
id   └──────────────┘      └┘         └─────────────┘ └┘              └┘ └┘ └┘
src  └──────────────┘        └┘           └─────────────┘                        └┘
typ  └──────────────┘      └┘         └─────────────┘ └┘              └┘ └┘ └┘
doc                          └┘
141    by refine quotient.sound _; filter_upwards [eq] assume a, congr_arg g
id               └────────────┘                                  └───────┘ 
src       └─────┘└────────────┘└┘  └──────────────┘  └┘      └──┘└───────┘ 
typ       └─────┘└────────────┘└┘  └──────────────┘  └┘      └──┘└───────┘
doc       └─────┘              └┘  └──────────────┘  └┘      └──┘          
txt       └─────┘              └┘  └──────────────┘  └┘      └──┘          
par       └─────┘              └┘  └──────────────┘  └┘      └──┘          
pid                           └┘                └┘        └──┘          
st       └───────────────────────────────────────────────────────────────────
142  
src  
typ  
doc  
txt  
par  
pid  
st   
143  @[simp] lemma comp_mk {γ : Type*} [measurable_space γ] (g : β → γ) (hg : measurable g)
id                                      └──────────────┘                   └────────┘ 
src                                     └──────────────┘                      └────────┘
typ                                     └──────────────┘                   └────────┘ 
doc    └──┘                                                                   └────────┘
144    (f : α → β) (hf) : comp g hg (mk f hf) = mk (g ∘ f) (measurable.comp hg hf) :=
id                      └──┘  └┘  └┘  └┘   └┘       └─────────────┘ └┘ └┘
src                       └──┘       └┘        └┘         └─────────────┘
typ                     └──┘  └┘  └┘  └┘   └┘       └─────────────┘ └┘ └┘
doc                       └──┘       └┘         └┘
145  rfl
id   └─┘
src  └─┘
typ  └─┘
146  
147  lemma comp_eq_mk_to_fun {γ : Type*} [measurable_space γ] (g : β → γ) (hg : measurable g) (f : α →ₘ β) :
id                                        └──────────────┘                   └────────┘         └┘ 
src                                       └──────────────┘                      └────────┘           └┘
typ                                       └──────────────┘                   └────────┘         └┘ 
doc                                                                             └────────┘           └┘
148    comp g hg f = mk (g ∘ f.to_fun) (hg.comp f.measurable) :=
id     └──┘  └┘   └┘    └─────┘   └┘└───┘ └─────────┘
src    └──┘         └┘      └─────┘     └───┘  └─────────┘
typ    └──┘  └┘   └┘    └─────┘   └┘└───┘ └─────────┘
doc    └──┘          └┘       └─────┘
149  by conv_lhs { rw [self_eq_mk f, comp_mk] }
id                     └────────┘   └─────┘
src     └─────────┘└──┘└────────┘ └┘└─────┘└┘└─
typ     └─────────┘└──┘└────────┘└┘└─────┘└┘└─
txt     └─────────┘└──┘           └┘       └┘└─
par     └─────────┘└──┘           └┘       └┘└─
pid             └────┘           └┘       └─┘
st     └─────────┘└───────────────┘└───────┘ 
150  
src  
typ  
txt  
par  
pid  
st   
151  lemma comp_to_fun {γ : Type*} [measurable_space γ] (g : β → γ) (hg : measurable g) (f : α →ₘ β) :
id                                  └──────────────┘                   └────────┘         └┘ 
src                                 └──────────────┘                      └────────┘           └┘
typ                                 └──────────────┘                   └────────┘         └┘ 
doc                                                                       └────────┘           └┘
152    ∀ₘ a, (comp g hg f).to_fun a = (g ∘ f.to_fun) a :=
id     └┘   └──┘  └┘  └────┘       └─────┘  
src    └┘    └──┘        └────┘          └─────┘
typ    └┘   └──┘  └┘  └────┘       └─────┘  
doc    └┘    └──┘        └────┘            └─────┘
153  by { rw comp_eq_mk_to_fun, apply all_ae_mk_to_fun }
id           └───────────────┘        └──────────────┘
src       └─┘└───────────────┘  └────┘└──────────────┘
typ       └─┘└───────────────┘  └────┘└──────────────┘
doc       └─┘                   └────┘                
txt       └─┘                   └────┘                
par       └─┘                   └────┘                
pid                                                 
st     └─────────────────────┘└───────────────────────┘└┘
154  
155  /-- Given a measurable function `g : β → γ → δ`, and almost everywhere equal functions
156      `[f₁] : α →ₘ β` and `[f₂] : α →ₘ γ`, return the equivalence class of the function
157      `λa, g (f₁ a) (f₂ a)`, i.e., the almost everywhere equal function
158      `[λa, g (f₁ a) (f₂ a)] : α →ₘ γ` -/
159  def comp₂ {γ δ : Type*} [measurable_space γ] [measurable_space δ]
id                            └──────────────┘    └──────────────┘ 
src                           └──────────────┘     └──────────────┘
typ                           └──────────────┘    └──────────────┘ 
160    (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α →ₘ β) (f₂ : α →ₘ γ) : α →ₘ δ :=
id                        └────────┘                     └┘          └┘      └┘ 
src                          └────────┘                           └┘            └┘        └┘
typ                       └────────┘                     └┘          └┘      └┘ 
doc                          └────────┘                              └┘            └┘        └┘
161  begin
st   └─────
162    refine quotient.lift_on₂ f₁ f₂ (λf₁ f₂, mk (λa, g (f₁.1 a) (f₂.1 a)) $ _) _,
id            └───────────────┘ └┘ └┘          └┘      
src    └─────┘└───────────────┘      └─────┘└┘  └─┘    └─┘ └┘   └─┘ └─┘ └───┘
typ    └─────┘└───────────────┘└┘└┘  └─────┘└┘  └─┘   └─┘ └┘   └─┘ └─┘ └───┘
doc    └─────┘                       └─────┘└┘  └─┘    └─┘ └┘   └─┘ └─┘ └───┘
txt    └─────┘                       └─────┘    └─┘    └─┘ └┘   └─┘ └─┘ └───┘
par    └─────┘                       └─────┘    └─┘    └─┘ └┘   └─┘ └─┘ └───┘
pid                                 └─────┘    └─┘    └─┘ └┘   └─┘ └─┘ └───┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
163    { exact measurable.comp hg (measurable.prod_mk f₁.2 f₂.2) },
id             └─────────────┘ └┘  └────────────────┘ └┘   └┘
src      └────┘└─────────────┘   └────────────────┘  └─┘  └──┘
typ      └────┘└─────────────┘└┘ └────────────────┘└┘└─┘└┘└──┘
doc      └────┘                                      └─┘  └──┘
txt      └────┘                                      └─┘  └──┘
par      └────┘                                      └─┘  └──┘
pid                                                 └─┘  └─┘
st   ───┘└──────────────────────────────────────────────────────┘└┘
164    { rintros ⟨f₁, hf₁⟩ ⟨f₂, hf₂⟩ ⟨g₁, hg₁⟩ ⟨g₂, hg₂⟩ h₁ h₂,
src      └───────────────────────────────────────────────────┘
typ      └───────────────────────────────────────────────────┘
doc      └───────────────────────────────────────────────────┘
txt      └───────────────────────────────────────────────────┘
par      └───────────────────────────────────────────────────┘
pid             └────────────────────────────────────────────┘
st   ────────────────────────────────────────────────────────┘└─
165      refine quotient.sound _,
id              └────────────┘
src      └─────┘└────────────┘└┘
typ      └─────┘└────────────┘└┘
doc      └─────┘              └┘
txt      └─────┘              └┘
par      └─────┘              └┘
pid                          └┘
st   ──────────────────────────┘└─
166      filter_upwards [h₁, h₂],
src      └──────────────┘  └┘  
typ      └──────────────┘  └┘  
doc      └──────────────┘  └┘  
txt      └──────────────┘  └┘  
par      └──────────────┘  └┘  
pid                    └┘  └┘  
st   ──────────────────────────┘└─
167      simp {contextual := tt} }
id                           └┘
src      └───┘ └────────────┘└┘└┘
typ      └───┘ └────────────┘└┘└┘
doc      └───┘ └────────────┘  └┘
txt      └───┘ └────────────┘  └┘
par      └───┘ └────────────┘  └┘
pid           └────────────┘  
st   ───────────────────────────┘└─
168  end
st   ──┘
169  
170  @[simp] lemma comp₂_mk_mk {γ δ : Type*} [measurable_space γ] [measurable_space δ]
id                                            └──────────────┘    └──────────────┘ 
src                                           └──────────────┘     └──────────────┘
typ                                           └──────────────┘    └──────────────┘ 
doc    └──┘
171    (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α → β) (f₂ : α → γ) (hf₁ hf₂) :
id                        └────────┘                                  
src                          └────────┘               
typ                       └────────┘                                  
doc                          └────────┘
172    comp₂ g hg (mk f₁ hf₁) (mk f₂ hf₂) =
id     └───┘  └┘  └┘ └┘ └─┘   └┘ └┘ └─┘  
src    └───┘       └┘          └┘         
typ    └───┘  └┘  └┘ └┘ └─┘   └┘ └┘ └─┘  
doc    └───┘       └┘          └┘
173      mk (λa, g (f₁ a) (f₂ a)) (measurable.comp hg (measurable.prod_mk hf₁ hf₂)) :=
id       └┘       └┘    └┘     └─────────────┘ └┘  └────────────────┘ └─┘ └─┘
src      └┘                        └─────────────┘     └────────────────┘
typ      └┘       └┘    └┘     └─────────────┘ └┘  └────────────────┘ └─┘ └─┘
doc      └┘
174  rfl
id   └─┘
src  └─┘
typ  └─┘
175  
176  lemma comp₂_eq_mk_to_fun {γ δ : Type*} [measurable_space γ] [measurable_space δ]
id                                           └──────────────┘    └──────────────┘ 
src                                          └──────────────┘     └──────────────┘
typ                                          └──────────────┘    └──────────────┘ 
177    (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α →ₘ β) (f₂ : α →ₘ γ) :
id                        └────────┘                     └┘          └┘ 
src                          └────────┘                           └┘            └┘
typ                       └────────┘                     └┘          └┘ 
doc                          └────────┘                              └┘            └┘
178    comp₂ g hg f₁ f₂ = mk (λa, g (f₁.to_fun a) (f₂.to_fun a))
id     └───┘  └┘ └┘ └┘  └┘       └┘└─────┘    └┘└─────┘ 
src    └───┘             └┘           └─────┘       └─────┘
typ    └───┘  └┘ └┘ └┘  └┘       └┘└─────┘    └┘└─────┘ 
doc    └───┘              └┘           └─────┘       └─────┘
179      (hg.comp (measurable.prod_mk f₁.measurable f₂.measurable)) :=
id        └┘└───┘  └────────────────┘ └┘└─────────┘ └┘└─────────┘
src         └───┘  └────────────────┘   └─────────┘   └─────────┘
typ       └┘└───┘  └────────────────┘ └┘└─────────┘ └┘└─────────┘
180  by conv_lhs { rw [self_eq_mk f₁, self_eq_mk f₂, comp₂_mk_mk] }
id                     └────────┘ └┘  └────────┘ └┘  └─────────┘
src     └─────────┘└──┘└────────┘  └┘└────────┘  └┘└─────────┘└┘└─
typ     └─────────┘└──┘└────────┘└┘└┘└────────┘└┘└┘└─────────┘└┘└─
txt     └─────────┘└──┘            └┘            └┘           └┘└─
par     └─────────┘└──┘            └┘            └┘           └┘└─
pid             └────┘            └┘            └┘           └─┘
st     └─────────┘└────────────────┘└─────────────┘└───────────┘ 
181  
src  
typ  
txt  
par  
pid  
st   
182  lemma comp₂_to_fun {γ δ : Type*} [measurable_space γ] [measurable_space δ]
id                                     └──────────────┘    └──────────────┘ 
src                                    └──────────────┘     └──────────────┘
typ                                    └──────────────┘    └──────────────┘ 
183    (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α →ₘ β) (f₂ : α →ₘ γ) :
id                        └────────┘                     └┘          └┘ 
src                          └────────┘                           └┘            └┘
typ                       └────────┘                     └┘          └┘ 
doc                          └────────┘                              └┘            └┘
184    ∀ₘ a, (comp₂ g hg f₁ f₂).to_fun a = g (f₁.to_fun a) (f₂.to_fun a) :=
id     └┘   └───┘  └┘ └┘ └┘ └────┘      └┘└─────┘    └┘└─────┘ 
src    └┘    └───┘            └────┘          └─────┘       └─────┘
typ    └┘   └───┘  └┘ └┘ └┘ └────┘      └┘└─────┘    └┘└─────┘ 
doc    └┘    └───┘            └────┘           └─────┘       └─────┘
185  by { rw comp₂_eq_mk_to_fun, apply all_ae_mk_to_fun }
id           └────────────────┘        └──────────────┘
src       └─┘└────────────────┘  └────┘└──────────────┘
typ       └─┘└────────────────┘  └────┘└──────────────┘
doc       └─┘                    └────┘                
txt       └─┘                    └────┘                
par       └─┘                    └────┘                
pid                                                  
st     └──────────────────────┘└───────────────────────┘└┘
186  
187  /-- Given a predicate `p` and an equivalence class `[f]`, return true if `p` holds of `f a`
188      for almost all `a` -/
189  def lift_pred (p : β → Prop) (f : α →ₘ β) : Prop :=
id                                     └┘ 
src                                      └┘
typ                                    └┘ 
doc                                      └┘
190  quotient.lift_on f (λf, ∀ₘ a, p (f.1 a))
id   └──────────────┘      └┘      
src  └──────────────┘        └┘       
typ  └──────────────┘      └┘      
doc                          └┘  
191  begin
st   └─────
192    assume f g h, dsimp, refine propext (all_ae_congr _),
id                                 └─────┘  └──────────┘
src    └──────────┘  └───┘  └─────┘└─────┘ └──────────┘└─┘
typ    └──────────┘  └───┘  └─────┘└─────┘ └──────────┘└─┘
doc    └──────────┘  └───┘  └─────┘                    └─┘
txt    └──────────┘  └───┘  └─────┘                    └─┘
par    └──────────┘  └───┘  └─────┘                    └─┘
pid    └──────────┘                                   └─┘
st   ─────────────┘└─────┘└───────────────────────────────┘└─
193    filter_upwards [h], simp {contextual := tt}
id                                             └┘
src    └──────────────┘   └───┘ └────────────┘└┘└┘
typ    └──────────────┘   └───┘ └────────────┘└┘└┘
doc    └──────────────┘   └───┘ └────────────┘  └┘
txt    └──────────────┘   └───┘ └────────────┘  └┘
par    └──────────────┘   └───┘ └────────────┘  └┘
pid                  └┘        └────────────┘  
st   ───────────────────┘└────────────────────────┘
194  end
st   └─┘
195  
196  /-- Given a relation `r` and equivalence class `[f]` and `[g]`, return true if `r` holds of
197      `(f a, g a)` for almost all `a` -/
198  def lift_rel {γ : Type*} [measurable_space γ] (r : β → γ → Prop) (f : α →ₘ β) (g : α →ₘ γ) : Prop :=
id                             └──────────────┘                          └┘         └┘ 
src                            └──────────────┘                              └┘           └┘
typ                            └──────────────┘                          └┘         └┘ 
doc                                                                          └┘           └┘
199  lift_pred (λp:β×γ, r p.1 p.2)
id   └───────┘          
src  └───────┘               
typ  └───────┘          
doc  └───────┘
200    (comp₂ prod.mk (measurable.prod_mk
id      └───┘ └─────┘  └────────────────┘
src     └───┘ └─────┘  └────────────────┘
typ     └───┘ └─────┘  └────────────────┘
doc     └───┘
201      (measurable.fst measurable_id) (measurable.snd measurable_id)) f g)
id        └────────────┘ └───────────┘   └────────────┘ └───────────┘    
src       └────────────┘ └───────────┘   └────────────┘ └───────────┘
typ       └────────────┘ └───────────┘   └────────────┘ └───────────┘    
202  
203  lemma lift_rel_mk_mk {γ : Type*} [measurable_space γ] (r : β → γ → Prop)
id                                     └──────────────┘           
src                                    └──────────────┘
typ                                    └──────────────┘           
204    (f : α → β) (g : α → γ) (hf hg) : lift_rel r (mk f hf) (mk g hg) ↔ ∀ₘ a, r (f a) (g a) :=
id                                   └──────┘   └┘  └┘   └┘  └┘   └┘         
src                                      └──────┘    └┘        └┘        └┘  
typ                                  └──────┘   └┘  └┘   └┘  └┘   └┘         
doc                                      └──────┘    └┘        └┘         └┘  
205  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
206  
207  lemma lift_rel_iff_to_fun {γ : Type*} [measurable_space γ] (r : β → γ → Prop) (f : α →ₘ β)
id                                          └──────────────┘                          └┘ 
src                                         └──────────────┘                              └┘
typ                                         └──────────────┘                          └┘ 
doc                                                                                       └┘
208    (g : α →ₘ γ) : lift_rel r f g ↔ ∀ₘ a, r (f.to_fun a) (g.to_fun a) :=
id           └┘     └──────┘     └┘    └─────┘    └─────┘ 
src           └┘      └──────┘        └┘       └─────┘      └─────┘
typ          └┘     └──────┘     └┘    └─────┘    └─────┘ 
doc           └┘      └──────┘         └┘       └─────┘      └─────┘
209  by conv_lhs { rw [self_eq_mk f, self_eq_mk g, lift_rel_mk_mk] }
id                     └────────┘   └────────┘   └────────────┘
src     └─────────┘└──┘└────────┘ └┘└────────┘ └┘└────────────┘└┘└─
typ     └─────────┘└──┘└────────┘└┘└────────┘└┘└────────────┘└┘└─
txt     └─────────┘└──┘           └┘           └┘              └┘└─
par     └─────────┘└──┘           └┘           └┘              └┘└─
pid             └────┘           └┘           └┘              └─┘
st     └─────────┘└───────────────┘└────────────┘└──────────────┘ 
210  
src  
typ  
txt  
par  
pid  
st   
211  section order
212  
213  instance [preorder β] : preorder (α →ₘ β) :=
id             └──────┘     └──────┘   └┘ 
src            └──────┘      └──────┘    └┘
typ            └──────┘     └──────┘   └┘ 
doc                                      └┘
214  { le          := lift_rel (≤),
id                   └──────┘ 
src                  └──────┘ 
typ                  └──────┘ 
doc                   └──────┘
215    le_refl     := by rintros ⟨⟨f, hf⟩⟩; exact univ_mem_sets' (assume a, le_refl _),
id                                                └────────────┘            └─────┘
src                      └───────────────┘  └────┘└────────────┘       └──┘└─────┘└─┘
typ                      └───────────────┘  └────┘└────────────┘       └──┘└─────┘└─┘
doc                      └───────────────┘  └────┘                     └──┘       └─┘
txt                      └───────────────┘  └────┘                     └──┘       └─┘
par                      └───────────────┘  └────┘                     └──┘       └─┘
pid                             └────────┘                            └──┘       └─┘
st                      └────────────────────────────────────────────────────────────┘
216    le_trans    :=
217    begin
st     └─────
218      rintros ⟨⟨f, hf⟩⟩ ⟨⟨g, hg⟩⟩ ⟨⟨h, hh⟩⟩ hfg hgh,
src      └───────────────────────────────────────────┘
typ      └───────────────────────────────────────────┘
doc      └───────────────────────────────────────────┘
txt      └───────────────────────────────────────────┘
par      └───────────────────────────────────────────┘
pid             └────────────────────────────────────┘
st   ────────────────────────────────────────────────┘└─
219      filter_upwards [hfg, hgh] assume a, le_trans
id                                           └──────┘
src      └──────────────┘   └┘   └┘      └──┘└──────┘
typ      └──────────────┘   └┘   └┘      └──┘└──────┘
doc      └──────────────┘   └┘   └┘      └──┘        
txt      └──────────────┘   └┘   └┘      └──┘        
par      └──────────────┘   └┘   └┘      └──┘        
pid                    └┘   └┘         └──┘        
st   ─────────────────────────────────────────────────
220    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
221  
222  lemma mk_le_mk [preorder β] {f g : α → β} (hf hg) : mk f hf ≤ mk g hg ↔ ∀ₘ a, f a ≤ g a :=
id                   └──────┘                         └┘  └┘  └┘  └┘  └┘      
src                  └──────┘                            └┘       └┘       └┘       
typ                  └──────┘                         └┘  └┘  └┘  └┘  └┘      
doc                                                      └┘        └┘        └┘  
223  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
224  
225  lemma le_iff_to_fun_le [preorder β] {f g : α →ₘ β} : f ≤ g ↔ ∀ₘ a, f.to_fun a ≤ g.to_fun a :=
id                           └──────┘           └┘         └┘  └─────┘   └─────┘ 
src                          └──────┘             └┘            └┘    └─────┘     └─────┘
typ                          └──────┘           └┘         └┘  └─────┘   └─────┘ 
doc                                               └┘              └┘    └─────┘      └─────┘
226  by { conv_lhs { rw [self_eq_mk f, self_eq_mk g] }, rw mk_le_mk }
id                       └────────┘   └────────┘         └──────┘
src       └─────────┘└──┘└────────┘ └┘└────────┘ └┘  └─┘└──────┘
typ       └─────────┘└──┘└────────┘└┘└────────┘└┘  └─┘└──────┘
doc                                                     └─┘        
txt       └─────────┘└──┘           └┘           └┘  └─┘        
par       └─────────┘└──┘           └┘           └┘  └─┘        
pid               └────┘           └┘           └─┘            
st     └───────────┘└───────────────┘└────────────┘ └┘└───────────┘└┘
227  
228  instance [partial_order β] : partial_order (α →ₘ β) :=
id             └───────────┘     └───────────┘   └┘ 
src            └───────────┘      └───────────┘    └┘
typ            └───────────┘     └───────────┘   └┘ 
doc                                                └┘
229  { le_antisymm :=
230    begin
st     └─────
231      rintros ⟨⟨f, hf⟩⟩ ⟨⟨g, hg⟩⟩ hfg hgf,
src      └─────────────────────────────────┘
typ      └─────────────────────────────────┘
doc      └─────────────────────────────────┘
txt      └─────────────────────────────────┘
par      └─────────────────────────────────┘
pid             └──────────────────────────┘
st   ──────────────────────────────────────┘└─
232      refine quotient.sound _,
id              └────────────┘
src      └─────┘└────────────┘└┘
typ      └─────┘└────────────┘└┘
doc      └─────┘              └┘
txt      └─────┘              └┘
par      └─────┘              └┘
pid                          └┘
st   ──────────────────────────┘└─
233      filter_upwards [hfg, hgf] assume a, le_antisymm
id                                           └─────────┘
src      └──────────────┘   └┘   └┘      └──┘└─────────┘
typ      └──────────────┘   └┘   └┘      └──┘└─────────┘
doc      └──────────────┘   └┘   └┘      └──┘           
txt      └──────────────┘   └┘   └┘      └──┘           
par      └──────────────┘   └┘   └┘      └──┘           
pid                    └┘   └┘         └──┘           
st   ────────────────────────────────────────────────────
234    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
235    .. ae_eq_fun.preorder }
id        └────────────────┘
src       └────────────────┘
typ       └────────────────┘
236  
237  /- TODO: Prove `L⁰` space is a lattice if β is linear order.
238           What if β is only a lattice? -/
239  
240  -- instance [linear_order β] : semilattice_sup (α →ₘ β) :=
241  -- { sup := comp₂ (⊔) (_),
242  --    .. ae_eq_fun.partial_order }
243  
244  end order
245  
246  variable (α)
247  /-- The equivalence class of a constant function: `[λa:α, b]`, based on the equivalence relation of
248      being almost everywhere equal -/
249  def const (b : β) : α →ₘ β := mk (λa:α, b) measurable_const
id                       └┘     └┘         └──────────────┘
src                        └┘      └┘           └──────────────┘
typ                      └┘     └┘         └──────────────┘
doc                        └┘      └┘
250  
251  lemma const_to_fun (b : β) : ∀ₘ a, (const α b).to_fun a = b := all_ae_mk_to_fun _ _
id                               └┘   └───┘   └────┘        └──────────────┘
src                               └┘    └───┘     └────┘          └──────────────┘
typ                              └┘   └───┘   └────┘        └──────────────┘
doc                               └┘    └───┘     └────┘
252  variable {α}
253  
254  instance [inhabited β] : inhabited (α →ₘ β) := ⟨const _ (default _)⟩
id             └───────┘     └───────┘   └┘       └───┘    └─────┘
src            └───────┘      └───────┘    └┘        └───┘    └─────┘
typ            └───────┘     └───────┘   └┘       └───┘    └─────┘
doc                                        └┘        └───┘
255  
256  instance [has_zero β] : has_zero (α →ₘ β) := ⟨const α 0⟩
id             └──────┘     └──────┘   └┘       └───┘ 
src            └──────┘      └──────┘    └┘        └───┘
typ            └──────┘     └──────┘   └┘       └───┘ 
doc                                      └┘        └───┘
257  lemma zero_def [has_zero β] : (0 : α →ₘ β) = mk (λa:α, 0) measurable_const := rfl
id                   └──────┘           └┘    └┘          └──────────────┘    └─┘
src                  └──────┘             └┘     └┘           └──────────────┘    └─┘
typ                  └──────┘           └┘    └┘          └──────────────┘    └─┘
doc                                       └┘      └┘
258  lemma zero_to_fun [has_zero β] : ∀ₘ a, (0 : α →ₘ β).to_fun a = 0 := const_to_fun _ _
id                      └──────┘     └┘        └┘  └────┘         └──────────┘
src                     └──────┘      └┘          └┘   └────┘          └──────────┘
typ                     └──────┘     └┘        └┘  └────┘         └──────────┘
doc                                   └┘          └┘   └────┘
259  
260  instance [has_one β] : has_one (α →ₘ β) := ⟨const α 1⟩
id             └─────┘     └─────┘   └┘       └───┘ 
src            └─────┘      └─────┘    └┘        └───┘
typ            └─────┘     └─────┘   └┘       └───┘ 
doc                                    └┘        └───┘
261  lemma one_def [has_one β] : (1 : α →ₘ β) = mk (λa:α, 1) measurable_const := rfl
id                  └─────┘           └┘    └┘          └──────────────┘    └─┘
src                 └─────┘             └┘     └┘           └──────────────┘    └─┘
typ                 └─────┘           └┘    └┘          └──────────────┘    └─┘
doc                                     └┘      └┘
262  lemma one_to_fun [has_one β] : ∀ₘ a, (1 : α →ₘ β).to_fun a = 1 := const_to_fun _ _
id                     └─────┘     └┘        └┘  └────┘         └──────────┘
src                    └─────┘      └┘          └┘   └────┘          └──────────┘
typ                    └─────┘     └┘        └┘  └────┘         └──────────┘
doc                                 └┘          └┘   └────┘
263  
264  section add_monoid
265  variables {γ : Type*}
266    [topological_space γ] [second_countable_topology γ] [add_monoid γ] [topological_add_monoid γ]
id      └───────────────┘     └───────────────────────┘     └────────┘     └────────────────────┘
src     └───────────────┘     └───────────────────────┘     └────────┘     └────────────────────┘
typ     └───────────────┘     └───────────────────────┘     └────────┘     └────────────────────┘
doc     └───────────────┘     └───────────────────────┘                    └────────────────────┘
267  
268  protected def add : (α →ₘ γ) → (α →ₘ γ) → (α →ₘ γ) :=
id                         └┘       └┘       └┘ 
src                         └┘         └┘         └┘
typ                        └┘       └┘       └┘ 
doc                         └┘         └┘         └┘
269  comp₂ (+) (measurable.add (measurable.fst measurable_id) (measurable.snd  measurable_id))
id   └───┘     └────────────┘  └────────────┘ └───────────┘   └────────────┘  └───────────┘
src  └───┘     └────────────┘  └────────────┘ └───────────┘   └────────────┘  └───────────┘
typ  └───┘     └────────────┘  └────────────┘ └───────────┘   └────────────┘  └───────────┘
doc  └───┘
270  
271  instance : has_add (α →ₘ γ) := ⟨ae_eq_fun.add⟩
id              └─────┘   └┘       └───────────┘
src             └─────┘    └┘        └───────────┘
typ             └─────┘   └┘       └───────────┘
doc                        └┘
272  
273  @[simp] lemma mk_add_mk (f g : α → γ) (hf hg) :
id                                     
typ                                    
doc    └──┘
274     (mk f hf) + (mk g hg) = mk (f + g) (measurable.add hf hg) := rfl
id       └┘  └┘    └┘  └┘   └┘       └────────────┘ └┘ └┘     └─┘
src      └┘         └┘        └┘         └────────────┘           └─┘
typ      └┘  └┘    └┘  └┘   └┘       └────────────┘ └┘ └┘     └─┘
doc      └┘          └┘         └┘
275  
276  lemma add_to_fun (f g : α →ₘ γ) : ∀ₘ a, (f + g).to_fun a = f.to_fun a + g.to_fun a :=
id                            └┘     └┘      └────┘    └─────┘   └─────┘ 
src                            └┘      └┘         └────┘      └─────┘     └─────┘
typ                           └┘     └┘      └────┘    └─────┘   └─────┘ 
doc                            └┘      └┘          └────┘       └─────┘      └─────┘
277  comp₂_to_fun _ _ _ _
id   └──────────┘
src  └──────────┘
typ  └──────────┘
278  
279  instance : add_monoid (α →ₘ γ) :=
id              └────────┘   └┘ 
src             └────────┘    └┘
typ             └────────┘   └┘ 
doc                           └┘
280  { zero      := 0,
281    add       := ae_eq_fun.add,
id                  └───────────┘
src                 └───────────┘
typ                 └───────────┘
282    add_zero  := by rintros ⟨a⟩; exact quotient.sound (univ_mem_sets' $ assume a, add_zero _),
id                                        └────────────┘  └────────────┘             └──────┘
src                    └─────────┘  └────┘└────────────┘ └────────────┘       └──┘└──────┘└─┘
typ                    └─────────┘  └────┘└────────────┘ └────────────┘       └──┘└──────┘└─┘
doc                    └─────────┘  └────┘                                    └──┘        └─┘
txt                    └─────────┘  └────┘                                    └──┘        └─┘
par                    └─────────┘  └────┘                                    └──┘        └─┘
pid                           └──┘                                           └──┘        └─┘
st                    └────────────────────────────────────────────────────────────────────────┘
283    zero_add  := by rintros ⟨a⟩; exact quotient.sound (univ_mem_sets' $ assume a, zero_add _),
id                                        └────────────┘  └────────────┘             └──────┘
src                    └─────────┘  └────┘└────────────┘ └────────────┘       └──┘└──────┘└─┘
typ                    └─────────┘  └────┘└────────────┘ └────────────┘       └──┘└──────┘└─┘
doc                    └─────────┘  └────┘                                    └──┘        └─┘
txt                    └─────────┘  └────┘                                    └──┘        └─┘
par                    └─────────┘  └────┘                                    └──┘        └─┘
pid                           └──┘                                           └──┘        └─┘
st                    └────────────────────────────────────────────────────────────────────────┘
284    add_assoc :=
285      by rintros ⟨a⟩ ⟨b⟩ ⟨c⟩; exact quotient.sound (univ_mem_sets' $ assume a, add_assoc _ _ _) }
id                                     └────────────┘  └────────────┘             └───────┘
src         └─────────────────┘  └────┘└────────────┘ └────────────┘       └──┘└───────┘└──────┘
typ         └─────────────────┘  └────┘└────────────┘ └────────────┘       └──┘└───────┘└──────┘
doc         └─────────────────┘  └────┘                                    └──┘         └──────┘
txt         └─────────────────┘  └────┘                                    └──┘         └──────┘
par         └─────────────────┘  └────┘                                    └──┘         └──────┘
pid                └──────────┘                                           └──┘         └─────┘
st         └──────────────────────────────────────────────────────────────────────────────────────┘
286  
287  end add_monoid
288  
289  section add_comm_monoid
290  variables {γ : Type*}
291    [topological_space γ] [second_countable_topology γ] [add_comm_monoid γ] [topological_add_monoid γ]
id      └───────────────┘     └───────────────────────┘     └─────────────┘     └────────────────────┘
src     └───────────────┘     └───────────────────────┘     └─────────────┘     └────────────────────┘
typ     └───────────────┘     └───────────────────────┘     └─────────────┘     └────────────────────┘
doc     └───────────────┘     └───────────────────────┘                         └────────────────────┘
292  
293  instance add_comm_monoid : add_comm_monoid (α →ₘ γ) :=
id                              └─────────────┘   └┘ 
src                             └─────────────┘    └┘
typ                             └─────────────┘   └┘ 
doc                                                └┘
294  { add_comm := by rintros ⟨a⟩ ⟨b⟩; exact quotient.sound (univ_mem_sets' $ assume a, add_comm _ _),
id                                           └────────────┘  └────────────┘             └──────┘
src                   └─────────────┘  └────┘└────────────┘ └────────────┘       └──┘└──────┘└───┘
typ                   └─────────────┘  └────┘└────────────┘ └────────────┘       └──┘└──────┘└───┘
doc                   └─────────────┘  └────┘                                    └──┘        └───┘
txt                   └─────────────┘  └────┘                                    └──┘        └───┘
par                   └─────────────┘  └────┘                                    └──┘        └───┘
pid                          └──────┘                                           └──┘        └───┘
st                   └──────────────────────────────────────────────────────────────────────────────┘
295    .. ae_eq_fun.add_monoid }
id        └──────────────────┘
src       └──────────────────┘
typ       └──────────────────┘
296  
297  end add_comm_monoid
298  
299  section add_group
300  
301  variables {γ : Type*} [topological_space γ] [add_group γ] [topological_add_group γ]
id                          └───────────────┘     └───────┘     └───────────────────┘
src                         └───────────────┘     └───────┘     └───────────────────┘
typ                         └───────────────┘     └───────┘     └───────────────────┘
doc                         └───────────────┘                   └───────────────────┘
302  
303  protected def neg : (α →ₘ γ) → (α →ₘ γ) := comp has_neg.neg (measurable.neg measurable_id)
id                         └┘       └┘      └──┘ └─────────┘  └────────────┘ └───────────┘
src                         └┘         └┘       └──┘ └─────────┘  └────────────┘ └───────────┘
typ                        └┘       └┘      └──┘ └─────────┘  └────────────┘ └───────────┘
doc                         └┘         └┘       └──┘
304  
305  instance : has_neg (α →ₘ γ) := ⟨ae_eq_fun.neg⟩
id              └─────┘   └┘       └───────────┘
src             └─────┘    └┘        └───────────┘
typ             └─────┘   └┘       └───────────┘
doc                        └┘
306  
307  @[simp] lemma neg_mk (f : α → γ) (hf) : -(mk f hf) = mk (-f) (measurable.neg hf) := rfl
id                                          └┘  └┘   └┘     └────────────┘ └┘     └─┘
src                                           └┘        └┘      └────────────┘        └─┘
typ                                         └┘  └┘   └┘     └────────────┘ └┘     └─┘
doc    └──┘                                    └┘         └┘
308  
309  lemma neg_to_fun (f : α →ₘ γ) : ∀ₘ a, (-f).to_fun a = - f.to_fun a := comp_to_fun _ _ _
id                          └┘     └┘    └────┘     └─────┘     └─────────┘
src                          └┘      └┘      └────┘       └─────┘      └─────────┘
typ                         └┘     └┘    └────┘     └─────┘     └─────────┘
doc                          └┘      └┘       └────┘         └─────┘
310  
311  variables [second_countable_topology γ]
id              └───────────────────────┘
src             └───────────────────────┘
typ             └───────────────────────┘
doc             └───────────────────────┘
312  instance : add_group (α →ₘ γ) :=
id              └───────┘   └┘ 
src             └───────┘    └┘
typ             └───────┘   └┘ 
doc                          └┘
313  { neg          := ae_eq_fun.neg,
id                     └───────────┘
src                    └───────────┘
typ                    └───────────┘
314    add_left_neg := by rintros ⟨a⟩; exact quotient.sound (univ_mem_sets' $ assume a, add_left_neg _),
id                                           └────────────┘  └────────────┘             └──────────┘
src                       └─────────┘  └────┘└────────────┘ └────────────┘       └──┘└──────────┘└─┘
typ                       └─────────┘  └────┘└────────────┘ └────────────┘       └──┘└──────────┘└─┘
doc                       └─────────┘  └────┘                                    └──┘            └─┘
txt                       └─────────┘  └────┘                                    └──┘            └─┘
par                       └─────────┘  └────┘                                    └──┘            └─┘
pid                              └──┘                                           └──┘            └─┘
st                       └────────────────────────────────────────────────────────────────────────────┘
315    .. ae_eq_fun.add_monoid
id        └──────────────────┘
src       └──────────────────┘
typ       └──────────────────┘
316   }
317  
318  @[simp] lemma mk_sub_mk (f g : α → γ) (hf hg) :
id                                     
typ                                    
doc    └──┘
319     (mk f hf) - (mk g hg) = mk (λa, (f a) - (g a)) (measurable.sub hf hg) := rfl
id       └┘  └┘    └┘  └┘   └┘                └────────────┘ └┘ └┘     └─┘
src      └┘         └┘        └┘                     └────────────┘           └─┘
typ      └┘  └┘    └┘  └┘   └┘                └────────────┘ └┘ └┘     └─┘
doc      └┘          └┘         └┘
320  
321  lemma sub_to_fun (f g : α →ₘ γ) : ∀ₘ a, (f - g).to_fun a = f.to_fun a - g.to_fun a :=
id                            └┘     └┘      └────┘    └─────┘   └─────┘ 
src                            └┘      └┘         └────┘      └─────┘     └─────┘
typ                           └┘     └┘      └────┘    └─────┘   └─────┘ 
doc                            └┘      └┘          └────┘       └─────┘      └─────┘
322  begin
st   └─────
323    rw sub_eq_add_neg,
id        └────────────┘
src    └─┘└────────────┘
typ    └─┘└────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────┘└─
324    filter_upwards [add_to_fun f (-g), neg_to_fun g],
id                     └────────┘      └────────┘ 
src    └──────────────┘└────────┘   └─┘└────────┘ 
typ    └──────────────┘└────────┘ └─┘└────────┘
doc    └──────────────┘              └─┘           
txt    └──────────────┘              └─┘           
par    └──────────────┘              └─┘           
pid                  └┘              └─┘           
st   ─────────────────────────────────────────────────┘└─
325    assume a,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
326    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
327    repeat {assume h, rw h},
id                          
src    └──────┘└──────┘└┘└─┘ 
typ    └──────┘└──────┘└┘└─┘
doc    └──────┘└──────┘└┘└─┘ 
txt    └──────┘└──────┘└┘└─┘ 
par    └──────┘└──────┘└┘└─┘ 
pid          └─────────────┘ 
st   ─────────────────┘└────┘└┘
328    refl
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
329  end
st   └─┘
330  
331  end add_group
332  
333  section add_comm_group
334  
335  variables {γ : Type*}
336    [topological_space γ] [second_countable_topology γ] [add_comm_group γ] [topological_add_group γ]
id      └───────────────┘     └───────────────────────┘     └────────────┘     └───────────────────┘
src     └───────────────┘     └───────────────────────┘     └────────────┘     └───────────────────┘
typ     └───────────────┘     └───────────────────────┘     └────────────┘     └───────────────────┘
doc     └───────────────┘     └───────────────────────┘                        └───────────────────┘
337  
338  instance : add_comm_group (α →ₘ γ) :=
id              └────────────┘   └┘ 
src             └────────────┘    └┘
typ             └────────────┘   └┘ 
doc                               └┘
339  { add_comm := ae_eq_fun.add_comm_monoid.add_comm
id                 └───────────────────────┘└───────┘
src                └───────────────────────┘└───────┘
typ                └───────────────────────┘└───────┘
340    .. ae_eq_fun.add_group
id        └─────────────────┘
src       └─────────────────┘
typ       └─────────────────┘
341  }
342  
343  end add_comm_group
344  
345  section semimodule
346  
347  variables {𝕜 : Type*} [semiring 𝕜] [topological_space 𝕜]
id                          └──────┘     └───────────────┘
src                         └──────┘     └───────────────┘
typ                         └──────┘     └───────────────┘
doc                                      └───────────────┘
348  variables {γ : Type*} [topological_space γ]
id                          └───────────────┘
src                         └───────────────┘
typ                         └───────────────┘
doc                         └───────────────┘
349            [add_comm_monoid γ] [semimodule 𝕜 γ] [topological_semimodule 𝕜 γ]
id              └─────────────┘     └────────┘       └────────────────────┘
src             └─────────────┘     └────────┘       └────────────────────┘
typ             └─────────────┘     └────────┘       └────────────────────┘
doc                                 └────────┘       └────────────────────┘
350  
351  protected def smul : 𝕜 → (α →ₘ γ) → (α →ₘ γ) :=
id                             └┘       └┘ 
src                              └┘         └┘
typ                            └┘       └┘ 
doc                              └┘         └┘
352  λ c f, comp (has_scalar.smul c) (measurable.smul _ measurable_id) f
id        └──┘  └─────────────┘    └─────────────┘   └───────────┘  
src         └──┘  └─────────────┘     └─────────────┘   └───────────┘
typ       └──┘  └─────────────┘    └─────────────┘   └───────────┘  
doc         └──┘
353  
354  instance : has_scalar 𝕜 (α →ₘ γ) := ⟨ae_eq_fun.smul⟩
id              └────────┘    └┘       └────────────┘
src             └────────┘      └┘        └────────────┘
typ             └────────┘    └┘       └────────────┘
doc             └────────┘      └┘
355  
356  @[simp] lemma smul_mk (c : 𝕜) (f : α → γ) (hf) : c • (mk f hf) = mk (c • f) (measurable.smul _ hf) :=
id                                                    └┘  └┘   └┘       └─────────────┘   └┘
src                                                       └┘        └┘         └─────────────┘
typ                                                   └┘  └┘   └┘       └─────────────┘   └┘
doc    └──┘                                                └┘         └┘
357  rfl
id   └─┘
src  └─┘
typ  └─┘
358  
359  lemma smul_to_fun (c : 𝕜) (f : α →ₘ γ) : ∀ₘ a, (c • f).to_fun a = c • f.to_fun a :=
id                                  └┘     └┘      └────┘      └─────┘ 
src                                   └┘      └┘         └────┘         └─────┘
typ                                 └┘     └┘      └────┘      └─────┘ 
doc                                   └┘      └┘          └────┘           └─────┘
360  comp_to_fun _ _ _
id   └─────────┘
src  └─────────┘
typ  └─────────┘
361  
362  variables [second_countable_topology γ] [topological_add_monoid γ]
id              └───────────────────────┘     └────────────────────┘
src             └───────────────────────┘     └────────────────────┘
typ             └───────────────────────┘     └────────────────────┘
doc             └───────────────────────┘     └────────────────────┘
363  
364  instance : semimodule 𝕜 (α →ₘ γ) :=
id              └────────┘    └┘ 
src             └────────┘      └┘
typ             └────────┘    └┘ 
doc             └────────┘      └┘
365  { one_smul  := by { rintros ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, one_smul] },
id                                                   └───────────┘  └─────┘  └──────┘
src                      └─────────────┘  └─────────┘└───────────┘└┘└─────┘└┘└──────┘└┘
typ                      └─────────────┘  └─────────┘└───────────┘└┘└─────┘└┘└──────┘└┘
doc                      └─────────────┘  └─────────┘             └┘       └┘        └┘
txt                      └─────────────┘  └─────────┘             └┘       └┘        └┘
par                      └─────────────┘  └─────────┘             └┘       └┘        └┘
pid                             └──────┘      └──┘└┘             └┘       └┘        
st                    └────────────────┘└─────────────────────────────────────────────┘└┘
366    mul_smul  :=
367      by { rintros x y ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, mul_action.mul_smul x y f], refl },
id                                            └───────────┘  └─────┘  └─────────────────┘   
src           └─────────────────┘  └─────────┘└───────────┘└┘└─────┘└┘└─────────────────┘     └───┘
typ           └─────────────────┘  └─────────┘└───────────┘└┘└─────┘└┘└─────────────────┘  └───┘
doc           └─────────────────┘  └─────────┘             └┘       └┘                        └───┘
txt           └─────────────────┘  └─────────┘             └┘       └┘                        └───┘
par           └─────────────────┘  └─────────┘             └┘       └┘                        └───┘
pid                  └──────────┘      └──┘└┘             └┘       └┘                            
st         └────────────────────┘└─────────────────────────────────────────────────────────────┘└─────┘└┘
368    smul_add  :=
369    begin
st     └─────
370      rintros x ⟨f, hf⟩ ⟨g, hg⟩, simp only [quot_mk_eq_mk, smul_mk, mk_add_mk],
id                                             └───────────┘  └─────┘  └───────┘
src      └───────────────────────┘  └─────────┘└───────────┘└┘└─────┘└┘└───────┘
typ      └───────────────────────┘  └─────────┘└───────────┘└┘└─────┘└┘└───────┘
doc      └───────────────────────┘  └─────────┘             └┘       └┘         
txt      └───────────────────────┘  └─────────┘             └┘       └┘         
par      └───────────────────────┘  └─────────┘             └┘       └┘         
pid             └────────────────┘      └──┘└┘             └┘       └┘         
st   ────────────────────────────┘└─────────────────────────────────────────────┘└─
371      congr, exact smul_add x f g
id                    └──────┘   
src      └───┘  └────┘└──────┘   
typ      └───┘  └────┘└──────┘
doc             └────┘           
txt      └───┘  └────┘           
par      └───┘  └────┘           
pid                             
st   ────────┘└──────────────────────
372    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
373    smul_zero := by { intro x, simp only [zero_def, smul_mk], congr, exact smul_zero x },
id                                           └──────┘  └─────┘                └───────┘ 
src                      └─────┘  └─────────┘└──────┘└┘└─────┘  └───┘  └────┘└───────┘ 
typ                      └─────┘  └─────────┘└──────┘└┘└─────┘  └───┘  └────┘└───────┘
doc                      └─────┘  └─────────┘        └┘                └────┘          
txt                      └─────┘  └─────────┘        └┘         └───┘  └────┘          
par                      └─────┘  └─────────┘        └┘         └───┘  └────┘          
pid                           └┘      └──┘└┘        └┘                               
st                    └────────┘└─────────────────────────────┘└─────┘└──────────────────┘└┘
374    add_smul  :=
375    begin
st     └─────
376      intros x y, rintro ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, mk_add_mk], congr,
id                                              └───────────┘  └─────┘  └───────┘
src      └────────┘  └────────────┘  └─────────┘└───────────┘└┘└─────┘└┘└───────┘  └───┘
typ      └────────┘  └────────────┘  └─────────┘└───────────┘└┘└─────┘└┘└───────┘  └───┘
doc      └────────┘  └────────────┘  └─────────┘             └┘       └┘         
txt      └────────┘  └────────────┘  └─────────┘             └┘       └┘           └───┘
par      └────────┘  └────────────┘  └─────────┘             └┘       └┘           └───┘
pid            └──┘        └──────┘      └──┘└┘             └┘       └┘         
st   ─────────────┘└──────────────┘└─────────────────────────────────────────────┘└─────┘└─
377      exact add_smul x y f
id             └──────┘   
src      └────┘└──────┘   
typ      └────┘└──────┘
doc      └────┘           
txt      └────┘           
par      └────┘           
pid                      
st   ─────────────────────────
378    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
379    zero_smul :=
380      by { rintro ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, zero_def], congr, exact zero_smul 𝕜 f }}
id                                       └───────────┘  └─────┘  └──────┘                └───────┘  
src           └────────────┘  └─────────┘└───────────┘└┘└─────┘└┘└──────┘  └───┘  └────┘└───────┘  
typ           └────────────┘  └─────────┘└───────────┘└┘└─────┘└┘└──────┘  └───┘  └────┘└───────┘
doc           └────────────┘  └─────────┘             └┘       └┘                 └────┘           
txt           └────────────┘  └─────────┘             └┘       └┘          └───┘  └────┘           
par           └────────────┘  └─────────┘             └┘       └┘          └───┘  └────┘           
pid                 └──────┘      └──┘└┘             └┘       └┘                                 
st         └───────────────┘└────────────────────────────────────────────┘└─────┘└────────────────────┘└┘
381  
382  instance : mul_action 𝕜 (α →ₘ γ) := by apply_instance
id              └────────┘    └┘ 
src             └────────┘      └┘          └──────────────
typ             └────────┘    └┘         └──────────────
doc             └────────┘      └┘          └──────────────
txt                                         └──────────────
par                                         └──────────────
pid                                                       
st                                         └───────────────
383  
src  
typ  
doc  
txt  
par  
pid  
st   
384  end semimodule
385  
386  section module
387  
388  variables {𝕜 : Type*} [ring 𝕜] [topological_space 𝕜]
id                          └──┘     └───────────────┘
src                         └──┘     └───────────────┘
typ                         └──┘     └───────────────┘
doc                                  └───────────────┘
389  variables {γ : Type*} [topological_space γ] [second_countable_topology γ] [add_comm_group γ]
id                          └───────────────┘     └───────────────────────┘     └────────────┘
src                         └───────────────┘     └───────────────────────┘     └────────────┘
typ                         └───────────────┘     └───────────────────────┘     └────────────┘
doc                         └───────────────┘     └───────────────────────┘
390            [topological_add_group γ] [module 𝕜 γ] [topological_semimodule 𝕜 γ]
id              └───────────────────┘     └────┘       └────────────────────┘
src             └───────────────────┘     └────┘       └────────────────────┘
typ             └───────────────────┘     └────┘       └────────────────────┘
doc             └───────────────────┘     └────┘       └────────────────────┘
391  
392  instance : module 𝕜 (α →ₘ γ) := { .. ae_eq_fun.semimodule }
id              └────┘    └┘           └──────────────────┘
src             └────┘      └┘            └──────────────────┘
typ             └────┘    └┘           └──────────────────┘
doc             └────┘      └┘
393  
394  end module
395  
396  section vector_space
397  
398  variables {𝕜 : Type*} [discrete_field 𝕜] [topological_space 𝕜]
id                          └────────────┘     └───────────────┘
src                         └────────────┘     └───────────────┘
typ                         └────────────┘     └───────────────┘
doc                                            └───────────────┘
399  variables {γ : Type*} [topological_space γ] [second_countable_topology γ] [add_comm_group γ]
id                          └───────────────┘     └───────────────────────┘     └────────────┘
src                         └───────────────┘     └───────────────────────┘     └────────────┘
typ                         └───────────────┘     └───────────────────────┘     └────────────┘
doc                         └───────────────┘     └───────────────────────┘
400            [topological_add_group γ] [vector_space 𝕜 γ] [topological_semimodule 𝕜 γ]
id              └───────────────────┘     └──────────┘       └────────────────────┘
src             └───────────────────┘     └──────────┘       └────────────────────┘
typ             └───────────────────┘     └──────────┘       └────────────────────┘
doc             └───────────────────┘     └──────────┘       └────────────────────┘
401  
402  instance : vector_space 𝕜 (α →ₘ γ) := { .. ae_eq_fun.semimodule }
id              └──────────┘    └┘           └──────────────────┘
src             └──────────┘      └┘            └──────────────────┘
typ             └──────────┘    └┘           └──────────────────┘
doc             └──────────┘      └┘
403  
404  end vector_space
405  
406  /- TODO : Prove that `L⁰` is a complete space if the codomain is complete. -/
407  /- TODO : Multiplicative structure of `L⁰` if useful -/
408  
409  open ennreal
410  
411  /-- For `f : α → ennreal`, Define `∫ [f]` to be `∫ f` -/
412  def eintegral (f : α →ₘ ennreal) : ennreal :=
id                       └┘ └─────┘    └─────┘
src                       └┘ └─────┘    └─────┘
typ                      └┘ └─────┘    └─────┘
doc                       └┘ └─────┘    └─────┘
413  quotient.lift_on f (λf, lintegral f.1) (assume ⟨f, hf⟩ ⟨g, hg⟩ eq, lintegral_congr_ae eq)
id   └──────────────┘      └───────┘                          └┘  └────────────────┘ └┘
src  └──────────────┘        └───────┘                             └┘  └────────────────┘ └┘
typ  └──────────────┘      └───────┘                          └┘  └────────────────┘ └┘
doc                          └───────┘
414  
415  @[simp] lemma eintegral_mk (f : α → ennreal) (hf) : eintegral (mk f hf) = lintegral f := rfl
id                                      └─────┘         └───────┘  └┘  └┘   └───────┘     └─┘
src                                      └─────┘         └───────┘  └┘        └───────┘      └─┘
typ                                     └─────┘         └───────┘  └┘  └┘   └───────┘     └─┘
doc    └──┘                              └─────┘         └───────┘  └┘         └───────┘
416  
417  lemma eintegral_to_fun (f : α →ₘ ennreal) : eintegral f = lintegral (f.to_fun) :=
id                                └┘ └─────┘    └───────┘   └───────┘  └─────┘
src                                └┘ └─────┘    └───────┘    └───────┘   └─────┘
typ                               └┘ └─────┘    └───────┘   └───────┘  └─────┘
doc                                └┘ └─────┘    └───────┘     └───────┘   └─────┘
418  by conv_lhs { rw [self_eq_mk f, eintegral_mk] }
id                     └────────┘   └──────────┘
src     └─────────┘└──┘└────────┘ └┘└──────────┘└┘└─
typ     └─────────┘└──┘└────────┘└┘└──────────┘└┘└─
txt     └─────────┘└──┘           └┘            └┘└─
par     └─────────┘└──┘           └┘            └┘└─
pid             └────┘           └┘            └─┘
st     └─────────┘└───────────────┘└────────────┘ 
419  
src  
typ  
txt  
par  
pid  
st   
420  @[simp] lemma eintegral_zero : eintegral (0 : α →ₘ ennreal) = 0 := lintegral_zero
id                                  └───────┘       └┘ └─────┘        └────────────┘
src                                 └───────┘        └┘ └─────┘        └────────────┘
typ                                 └───────┘       └┘ └─────┘        └────────────┘
doc    └──┘                         └───────┘        └┘ └─────┘
421  
422  @[simp] lemma eintegral_eq_zero_iff (f : α →ₘ ennreal) : eintegral f = 0 ↔ f = 0 :=
id                                             └┘ └─────┘    └───────┘       
src                                             └┘ └─────┘    └───────┘         
typ                                            └┘ └─────┘    └───────┘       
doc    └──┘                                     └┘ └─────┘    └───────┘
423  begin
st   └─────
424    rcases f with ⟨f, hf⟩,
id            
src    └─────┘ └───────────┘
typ    └─────┘└───────────┘
doc    └─────┘ └───────────┘
txt    └─────┘ └───────────┘
par    └─────┘ └───────────┘
pid           └───────────┘
st   ──────────────────────┘└─
425    refine iff.trans (lintegral_eq_zero_iff hf) ⟨_, _⟩,
id            └───────┘  └───────────────────┘ └┘
src    └─────┘└───────┘ └───────────────────┘  └┘ └───┘
typ    └─────┘└───────┘ └───────────────────┘└┘└┘ └───┘
doc    └─────┘                                 └┘ └───┘
txt    └─────┘                                 └┘ └───┘
par    └─────┘                                 └┘ └───┘
pid                                           └┘ └───┘
st   ───────────────────────────────────────────────────┘└─
426    { assume h, exact quotient.sound h },
id                       └────────────┘ 
src      └──────┘  └────┘└────────────┘ 
typ      └──────┘  └────┘└────────────┘
doc      └──────┘  └────┘               
txt      └──────┘  └────┘               
par      └──────┘  └────┘               
pid      └──────┘                      
st   ───┘└──────┘└───────────────────────┘└┘
427    { assume h, exact quotient.exact h }
id                       └────────────┘ 
src      └──────┘  └────┘└────────────┘ 
typ      └──────┘  └────┘└────────────┘
doc      └──────┘  └────┘               
txt      └──────┘  └────┘               
par      └──────┘  └────┘               
pid      └──────┘                      
st   ───────────┘└───────────────────────┘└─
428  end
st   ──┘
429  
430  lemma eintegral_add : ∀(f g : α →ₘ ennreal), eintegral (f + g) = eintegral f + eintegral g :=
id                                  └┘ └─────┘   └───────┘       └───────┘   └───────┘ 
src                                  └┘ └─────┘   └───────┘         └───────┘    └───────┘
typ                                 └┘ └─────┘   └───────┘       └───────┘   └───────┘ 
doc                                  └┘ └─────┘   └───────┘           └───────┘     └───────┘
431  by { rintros ⟨f⟩ ⟨g⟩, simp only [quot_mk_eq_mk, mk_add_mk, eintegral_mk], exact lintegral_add f.2 g.2 }
id                                    └───────────┘  └───────┘  └──────────┘         └───────────┘    
src       └─────────────┘  └─────────┘└───────────┘└┘└───────┘└┘└──────────┘  └────┘└───────────┘ └─┘ └─┘
typ       └─────────────┘  └─────────┘└───────────┘└┘└───────┘└┘└──────────┘  └────┘└───────────┘└─┘└─┘
doc       └─────────────┘  └─────────┘             └┘         └┘              └────┘              └─┘ └─┘
txt       └─────────────┘  └─────────┘             └┘         └┘              └────┘              └─┘ └─┘
par       └─────────────┘  └─────────┘             └┘         └┘              └────┘              └─┘ └─┘
pid              └──────┘      └──┘└┘             └┘         └┘                                 └─┘ └─┘
st     └────────────────┘└──────────────────────────────────────────────────┘└────────────────────────────┘└┘
432  
433  lemma eintegral_le_eintegral {f g : α →ₘ ennreal} (h : f ≤ g) : eintegral f ≤ eintegral g :=
id                                        └┘ └─────┘             └───────┘   └───────┘ 
src                                        └┘ └─────┘               └───────┘    └───────┘
typ                                       └┘ └─────┘             └───────┘   └───────┘ 
doc                                        └┘ └─────┘                └───────┘     └───────┘
434  begin
st   └─────
435    rcases f with ⟨f, hf⟩, rcases g with ⟨g, hg⟩,
id                                  
src    └─────┘ └───────────┘  └─────┘ └───────────┘
typ    └─────┘└───────────┘  └─────┘└───────────┘
doc    └─────┘ └───────────┘  └─────┘ └───────────┘
txt    └─────┘ └───────────┘  └─────┘ └───────────┘
par    └─────┘ └───────────┘  └─────┘ └───────────┘
pid           └───────────┘         └───────────┘
st   ──────────────────────┘└─────────────────────┘└─
436    simp only [quot_mk_eq_mk, eintegral_mk, mk_le_mk] at *,
id                └───────────┘  └──────────┘  └──────┘
src    └─────────┘└───────────┘└┘└──────────┘└┘└──────┘└────┘
typ    └─────────┘└───────────┘└┘└──────────┘└┘└──────┘└────┘
doc    └─────────┘             └┘            └┘        └────┘
txt    └─────────┘             └┘            └┘        └────┘
par    └─────────┘             └┘            └┘        └────┘
pid        └──┘└┘             └┘            └┘        └──┘
st   ───────────────────────────────────────────────────────┘└─
437    refine lintegral_le_lintegral_ae _,
id            └───────────────────────┘
src    └─────┘└───────────────────────┘└┘
typ    └─────┘└───────────────────────┘└┘
doc    └─────┘                         └┘
txt    └─────┘                         └┘
par    └─────┘                         └┘
pid                                   └┘
st   ───────────────────────────────────┘└─
438    filter_upwards [h], simp
src    └──────────────┘   └───┘
typ    └──────────────┘   └───┘
doc    └──────────────┘   └───┘
txt    └──────────────┘   └───┘
par    └──────────────┘   └───┘
pid                  └┘       
st   ───────────────────┘└─────┘
439  end
st   └─┘
440  
441  section
442  variables {γ : Type*} [emetric_space γ] [second_countable_topology γ]
id                          └───────────┘     └───────────────────────┘
src                         └───────────┘     └───────────────────────┘
typ                         └───────────┘     └───────────────────────┘
doc                         └───────────┘     └───────────────────────┘
443  
444  /-- `comp_edist [f] [g] a` will return `edist (f a) (g a) -/
445  def comp_edist (f g : α →ₘ γ) : α →ₘ ennreal := comp₂ edist measurable_edist f g
id                          └┘      └┘ └─────┘    └───┘ └───┘ └──────────────┘  
src                          └┘        └┘ └─────┘    └───┘ └───┘ └──────────────┘
typ                         └┘      └┘ └─────┘    └───┘ └───┘ └──────────────┘  
doc                          └┘        └┘ └─────┘    └───┘
446  
447  lemma comp_edist_to_fun (f g : α →ₘ γ) :
id                                   └┘ 
src                                   └┘
typ                                  └┘ 
doc                                   └┘
448    ∀ₘ a, (comp_edist f g).to_fun a = edist (f.to_fun a) (g.to_fun a) :=
id     └┘   └────────┘   └────┘    └───┘  └─────┘    └─────┘ 
src    └┘    └────────┘     └────┘     └───┘   └─────┘      └─────┘
typ    └┘   └────────┘   └────┘    └───┘  └─────┘    └─────┘ 
doc    └┘    └────────┘     └────┘              └─────┘      └─────┘
449  comp₂_to_fun _ _ _ _
id   └──────────┘
src  └──────────┘
typ  └──────────┘
450  
451  lemma comp_edist_self : ∀ (f : α →ₘ γ), comp_edist f f = 0 :=
id                                   └┘    └────────┘   
src                                   └┘     └────────┘     
typ                                  └┘    └────────┘   
doc                                   └┘     └────────┘
452  by rintro ⟨f⟩; refine quotient.sound _; simp only [edist_self]
id                         └────────────┘               └────────┘
src     └────────┘  └─────┘└────────────┘└┘  └─────────┘└────────┘└─
typ     └────────┘  └─────┘└────────────┘└┘  └─────────┘└────────┘└─
doc     └────────┘  └─────┘              └┘  └─────────┘          └─
txt     └────────┘  └─────┘              └┘  └─────────┘          └─
par     └────────┘  └─────┘              └┘  └─────────┘          └─
pid           └──┘                      └┘      └──┘└┘          
st     └────────────────────────────────────────────────────────────
453  
src  
typ  
doc  
txt  
par  
pid  
st   
454  /-- Almost everywhere equal functions form an `emetric_space`, with the emetric defined as
455    `edist f g = ∫⁻ a, edist (f a) (g a)`. -/
456  instance : emetric_space (α →ₘ γ) :=
id              └───────────┘   └┘ 
src             └───────────┘    └┘
typ             └───────────┘   └┘ 
doc             └───────────┘    └┘
457  { edist               := λf g, eintegral (comp_edist f g),
id                               └───────┘  └────────┘  
src                                └───────┘  └────────┘
typ                              └───────┘  └────────┘  
doc                                 └───────┘  └────────┘
458    edist_self          := assume f, (eintegral_eq_zero_iff _).2 (comp_edist_self _),
id                                      └───────────────────┘      └─────────────┘
src                                      └───────────────────┘      └─────────────┘
typ                                     └───────────────────┘      └─────────────┘
459    edist_comm          :=
460      by rintros ⟨f⟩ ⟨g⟩; simp only [comp_edist, quot_mk_eq_mk, comp₂_mk_mk, edist_comm],
id                                      └────────┘  └───────────┘  └─────────┘  └────────┘
src         └─────────────┘  └─────────┘└────────┘└┘└───────────┘└┘└─────────┘└┘└────────┘
typ         └─────────────┘  └─────────┘└────────┘└┘└───────────┘└┘└─────────┘└┘└────────┘
doc         └─────────────┘  └─────────┘└────────┘└┘             └┘           └┘          
txt         └─────────────┘  └─────────┘          └┘             └┘           └┘          
par         └─────────────┘  └─────────┘          └┘             └┘           └┘          
pid                └──────┘      └──┘└┘          └┘             └┘           └┘          
st         └──────────────────────────────────────────────────────────────────────────────┘
461    edist_triangle      :=
462    begin
st     └─────
463      rintros ⟨f⟩ ⟨g⟩ ⟨h⟩,
src      └─────────────────┘
typ      └─────────────────┘
doc      └─────────────────┘
txt      └─────────────────┘
par      └─────────────────┘
pid             └──────────┘
st   ──────────────────────┘└─
464      simp only [comp_edist, quot_mk_eq_mk, comp₂_mk_mk, (eintegral_add _ _).symm],
id                  └────────┘  └───────────┘  └─────────┘   └───────────┘
src      └─────────┘└────────┘└┘└───────────┘└┘└─────────┘└┘ └───────────┘└─────────┘
typ      └─────────┘└────────┘└┘└───────────┘└┘└─────────┘└┘ └───────────┘└─────────┘
doc      └─────────┘└────────┘└┘             └┘           └┘              └─────────┘
txt      └─────────┘          └┘             └┘           └┘              └─────────┘
par      └─────────┘          └┘             └┘           └┘              └─────────┘
pid          └──┘└┘          └┘             └┘           └┘              └─────────┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
465      exact lintegral_le_lintegral _ _ (assume a, edist_triangle _ _ _)
id             └────────────────────┘                └────────────┘
src      └────┘└────────────────────┘└───┘       └──┘└────────────┘└───────
typ      └────┘└────────────────────┘└───┘       └──┘└────────────┘└───────
doc      └────┘                      └───┘       └──┘              └───────
txt      └────┘                      └───┘       └──┘              └───────
par      └────┘                      └───┘       └──┘              └───────
pid                                 └───┘       └──┘              └─────┘
st   ──────────────────────────────────────────────────────────────────────
466    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
467    eq_of_edist_eq_zero :=
468    begin
st     └─────
469      rintros ⟨f⟩ ⟨g⟩,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid             └──────┘
st   ──────────────────┘└─
470      simp only [edist, comp_edist, quot_mk_eq_mk, comp₂_mk_mk, eintegral_eq_zero_iff],
id                         └────────┘  └───────────┘  └─────────┘  └───────────────────┘
src      └─────────┘     └┘└────────┘└┘└───────────┘└┘└─────────┘└┘└───────────────────┘
typ      └─────────┘     └┘└────────┘└┘└───────────┘└┘└─────────┘└┘└───────────────────┘
doc      └─────────┘     └┘└────────┘└┘             └┘           └┘                     
txt      └─────────┘     └┘          └┘             └┘           └┘                     
par      └─────────┘     └┘          └┘             └┘           └┘                     
pid          └──┘└┘     └┘          └┘             └┘           └┘                     
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
471      simp only [zero_def, mk_eq_mk, edist_eq_zero],
id                  └──────┘  └──────┘  └───────────┘
src      └─────────┘└──────┘└┘└──────┘└┘└───────────┘
typ      └─────────┘└──────┘└┘└──────┘└┘└───────────┘
doc      └─────────┘        └┘        └┘└───────────┘
txt      └─────────┘        └┘        └┘             
par      └─────────┘        └┘        └┘             
pid          └──┘└┘        └┘        └┘             
st   ────────────────────────────────────────────────┘└─
472      assume h, assumption
src      └──────┘  └──────────
typ      └──────┘  └──────────
doc      └──────┘  └──────────
txt      └──────┘  └──────────
par      └──────┘  └──────────
pid      └──────┘            
st   ───────────┘└────────────
473    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
474  
475  lemma edist_mk_mk {f g : α → γ} (hf hg) : edist (mk f hf) (mk g hg) = ∫⁻ x, edist (f x) (g x) := rfl
id                                           └───┘  └┘  └┘   └┘  └┘   └┘  └───┘            └─┘
src                                            └───┘  └┘        └┘        └┘   └───┘                └─┘
typ                                          └───┘  └┘  └┘   └┘  └┘   └┘  └───┘            └─┘
doc                                                   └┘        └┘         └┘  
476  
477  lemma edist_to_fun (f g : α →ₘ γ) : edist f g = ∫⁻ x, edist (f.to_fun x) (g.to_fun x) :=
id                              └┘     └───┘    └┘  └───┘  └─────┘    └─────┘ 
src                              └┘      └───┘      └┘   └───┘   └─────┘      └─────┘
typ                             └┘     └───┘    └┘  └───┘  └─────┘    └─────┘ 
doc                              └┘                  └┘           └─────┘      └─────┘
478  by conv_lhs { rw [self_eq_mk f, self_eq_mk g, edist_mk_mk] }
id                     └────────┘   └────────┘   └─────────┘
src     └─────────┘└──┘└────────┘ └┘└────────┘ └┘└─────────┘└┘└─
typ     └─────────┘└──┘└────────┘└┘└────────┘└┘└─────────┘└┘└─
txt     └─────────┘└──┘           └┘           └┘           └┘└─
par     └─────────┘└──┘           └┘           └┘           └┘└─
pid             └────┘           └┘           └┘           └─┘
st     └─────────┘└───────────────┘└────────────┘└───────────┘ 
479  
src  
typ  
txt  
par  
pid  
st   
480  lemma edist_zero_to_fun [has_zero γ] (f : α →ₘ γ) : edist f 0 = ∫⁻ x, edist (f.to_fun x) 0 :=
id                            └──────┘         └┘     └───┘     └┘  └───┘  └─────┘ 
src                           └──────┘           └┘      └───┘      └┘   └───┘   └─────┘
typ                           └──────┘         └┘     └───┘     └┘  └───┘  └─────┘ 
doc                                              └┘                  └┘           └─────┘
481  begin
st   └─────
482    rw edist_to_fun,
id        └──────────┘
src    └─┘└──────────┘
typ    └─┘└──────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────┘└─
483    apply lintegral_congr_ae,
id           └────────────────┘
src    └────┘└────────────────┘
typ    └────┘└────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────┘└─
484    have : ∀ₘ a:α, (0 : α →ₘ γ).to_fun a = 0 := zero_to_fun,
id            └┘           └┘                  └─────────┘
src    └─────┘└┘└─┘  └──┘ └┘ └───────┘ └────┘└─────────┘
typ    └─────┘└┘└─┘  └──┘└┘└───────┘ └────┘└─────────┘
doc    └─────┘└┘└─┘  └──┘ └┘ └───────┘  └────┘
txt    └─────┘  └─┘   └──┘    └───────┘  └────┘
par    └─────┘  └─┘   └──┘    └───────┘  └────┘
pid    └───┘└┘  └─┘   └──┘    └───────┘  └───┘
st   ────────────────────────────────────────────────────────┘└─
485    filter_upwards [this],
src    └──────────────┘    
typ    └──────────────┘    
doc    └──────────────┘    
txt    └──────────────┘    
par    └──────────────┘    
pid                  └┘    
st   ──────────────────────┘└─
486    assume a h,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid    └────────┘
st   ───────────┘└─
487    simp only [mem_set_of_eq] at *,
id                └───────────┘
src    └─────────┘└───────────┘└────┘
typ    └─────────┘└───────────┘└────┘
doc    └─────────┘             └────┘
txt    └─────────┘             └────┘
par    └─────────┘             └────┘
pid        └──┘└┘             └──┘
st   ───────────────────────────────┘└─
488    rw h
id        
src    └─┘ 
typ    └─┘
doc    └─┘ 
txt    └─┘ 
par    └─┘ 
pid       
st   ──────┘
489  end
st   └─┘
490  
491  end
492  
493  section metric
494  variables {γ : Type*} [metric_space γ] [second_countable_topology γ]
id                          └──────────┘     └───────────────────────┘
src                         └──────────┘     └───────────────────────┘
typ                         └──────────┘     └───────────────────────┘
doc                         └──────────┘     └───────────────────────┘
495  
496  lemma edist_mk_mk' {f g : α → γ} (hf hg) :
id                                
typ                               
497    edist (mk f hf) (mk g hg) = ∫⁻ x, nndist (f x) (g x) :=
id     └───┘  └┘  └┘   └┘  └┘   └┘  └────┘       
src    └───┘  └┘        └┘        └┘   └────┘
typ    └───┘  └┘  └┘   └┘  └┘   └┘  └────┘       
doc           └┘        └┘         └┘   └────┘
498  show  (∫⁻ x, edist (f x) (g x)) =  ∫⁻ x, nndist (f x) (g x), from
id          └┘  └───┘            └┘  └────┘       
src         └┘   └───┘                └┘   └────┘
typ         └┘  └───┘            └┘  └────┘       
doc         └┘                         └┘   └────┘
499  lintegral_congr_ae $all_ae_of_all $ assume a, edist_nndist _ _
id   └────────────────┘  └───────────┘            └──────────┘
src  └────────────────┘  └───────────┘             └──────────┘
typ  └────────────────┘  └───────────┘            └──────────┘
doc                                                └──────────┘
500  
501  lemma edist_to_fun' (f g : α →ₘ γ) : edist f g = ∫⁻ x, nndist (f.to_fun x) (g.to_fun x) :=
id                               └┘     └───┘    └┘  └────┘  └─────┘    └─────┘ 
src                               └┘      └───┘      └┘   └────┘   └─────┘      └─────┘
typ                              └┘     └───┘    └┘  └────┘  └─────┘    └─────┘ 
doc                               └┘                  └┘   └────┘   └─────┘      └─────┘
502  by conv_lhs { rw [self_eq_mk f, self_eq_mk g, edist_mk_mk'] }
id                     └────────┘   └────────┘   └──────────┘
src     └─────────┘└──┘└────────┘ └┘└────────┘ └┘└──────────┘└┘└─
typ     └─────────┘└──┘└────────┘└┘└────────┘└┘└──────────┘└┘└─
txt     └─────────┘└──┘           └┘           └┘            └┘└─
par     └─────────┘└──┘           └┘           └┘            └┘└─
pid             └────┘           └┘           └┘            └─┘
st     └─────────┘└───────────────┘└────────────┘└────────────┘ 
503  
src  
typ  
txt  
par  
pid  
st   
504  end metric
505  
506  section normed_group
507  
508  variables {γ : Type*} [normed_group γ] [second_countable_topology γ]
id                          └──────────┘     └───────────────────────┘
src                         └──────────┘     └───────────────────────┘
typ                         └──────────┘     └───────────────────────┘
doc                         └──────────┘     └───────────────────────┘
509  
510  lemma edist_eq_add_add : ∀ {f g h : α →ₘ γ}, edist f g = edist (f + h) (g + h) :=
id                                        └┘    └───┘    └───┘         
src                                        └┘     └───┘      └───┘           
typ                                       └┘    └───┘    └───┘         
doc                                        └┘
511  begin
st   └─────
512    rintros ⟨f⟩ ⟨g⟩ ⟨h⟩,
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid           └──────────┘
st   ────────────────────┘└─
513    simp only [quot_mk_eq_mk, mk_add_mk, edist_mk_mk'],
id                └───────────┘  └───────┘  └──────────┘
src    └─────────┘└───────────┘└┘└───────┘└┘└──────────┘
typ    └─────────┘└───────────┘└┘└───────┘└┘└──────────┘
doc    └─────────┘             └┘         └┘            
txt    └─────────┘             └┘         └┘            
par    └─────────┘             └┘         └┘            
pid        └──┘└┘             └┘         └┘            
st   ───────────────────────────────────────────────────┘└─
514    apply lintegral_congr_ae,
id           └────────────────┘
src    └────┘└────────────────┘
typ    └────┘└────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────┘└─
515    filter_upwards [], simp [nndist_eq_nnnorm]
id                              └──────────────┘
src    └───────────────┘  └────┘└──────────────┘└┘
typ    └───────────────┘  └────┘└──────────────┘└┘
doc    └───────────────┘  └────┘                └┘
txt    └───────────────┘  └────┘                └┘
par    └───────────────┘  └────┘                └┘
pid                  └─┘                      
st   ──────────────────┘└────────────────────────┘
516  end
st   └─┘
517  
518  end normed_group
519  
520  section normed_space
521  
522  set_option class.instance_max_depth 100
doc             └──────────────────────┘
523  
524  variables {𝕜 : Type*} [normed_field 𝕜]
id                          └──────────┘
src                         └──────────┘
typ                         └──────────┘
doc                         └──────────┘
525  variables {γ : Type*} [normed_group γ] [second_countable_topology γ] [normed_space 𝕜 γ]
id                          └──────────┘     └───────────────────────┘     └──────────┘
src                         └──────────┘     └───────────────────────┘     └──────────┘
typ                         └──────────┘     └───────────────────────┘     └──────────┘
doc                         └──────────┘     └───────────────────────┘     └──────────┘
526  
527  lemma edist_smul (x : 𝕜) : ∀ f : α →ₘ γ, edist (x • f) 0 = (ennreal.of_real ∥x∥) * edist f 0 :=
id                                    └┘   └───┘          └─────────────┘    └───┘ 
src                                     └┘    └───┘            └─────────────┘     └───┘
typ                                   └┘   └───┘          └─────────────┘    └───┘ 
doc                                     └┘                       └─────────────┘
528  begin
st   └─────
529    rintros ⟨f, hf⟩, simp only [zero_def, edist_mk_mk', quot_mk_eq_mk, smul_mk],
id                                 └──────┘  └──────────┘  └───────────┘  └─────┘
src    └─────────────┘  └─────────┘└──────┘└┘└──────────┘└┘└───────────┘└┘└─────┘
typ    └─────────────┘  └─────────┘└──────┘└┘└──────────┘└┘└───────────┘└┘└─────┘
doc    └─────────────┘  └─────────┘        └┘            └┘             └┘       
txt    └─────────────┘  └─────────┘        └┘            └┘             └┘       
par    └─────────────┘  └─────────┘        └┘            └┘             └┘       
pid           └──────┘      └──┘└┘        └┘            └┘             └┘       
st   ────────────────┘└──────────────────────────────────────────────────────────┘└─
530    exact calc
src    └────┘    
typ    └────┘    
doc    └────┘    
txt    └────┘    
par    └────┘    
pid             
st   ─────────────
531      (∫⁻ (a : α), nndist (x • f a) 0) = (∫⁻ (a : α), (nnnorm x) * nnnorm (f a)) :
id        └┘         └────┘                                      └────┘  
src  ───┘ └┘└────┘ └────┘    └───┘    └────┘          └┘└────┘   └────
typ  ───┘ └┘└────┘ └────┘    └───┘    └────┘        └┘└────┘  └────
doc  ───┘ └┘└────┘ └────┘     └───┘    └────┘          └┘ └────┘   └────
txt  ───┘   └────┘             └───┘    └────┘          └┘          └────
par  ───┘   └────┘             └───┘    └────┘          └┘          └────
pid  ───┘   └────┘             └───┘    └────┘          └┘          └────
st   ─────────────────────────────────────────────────────────────────────────────────
532        lintegral_congr_ae $ by { filter_upwards [], assume a, simp [nndist_eq_nnnorm, nnnorm_smul] }
id         └────────────────┘                                           └──────────────┘  └─────────┘
src  ─────┘└────────────────┘   └─┘└───────────────┘└┘└──────┘└┘└────┘└──────────────┘└┘└─────────┘└┘└─
typ  ─────┘└────────────────┘   └─┘└───────────────┘└┘└──────┘└┘└────┘└──────────────┘└┘└─────────┘└┘└─
doc  ─────┘                     └─┘└───────────────┘└┘└──────┘└┘└────┘                └┘           └┘└─
txt  ─────┘                     └─┘└───────────────┘└┘└──────┘└┘└────┘                └┘           └┘└─
par  ─────┘                     └─┘└───────────────┘└┘└──────┘└┘└────┘                └┘           └┘└─
pid  ─────┘                     └────────────────────────────────────┘                └┘           └───
st   ────────────────────────────┘└──────────────────┘└────────┘└─────────────────────────────────────┘
533      ... = _ : lintegral_const_mul _ (measurable.coe_nnnorm hf)
id                 └─────────────────┘    └───────────────────┘ └┘
src  ───────┘ └───┘└─────────────────┘└─┘ └───────────────────┘  └─
typ  ───────┘ └───┘└─────────────────┘└─┘ └───────────────────┘└┘└─
doc  ───────┘ └───┘                   └─┘                        └─
txt  ───────┘ └───┘                   └─┘                        └─
par  ───────┘ └───┘                   └─┘                        └─
pid  ───────┘ └───┘                   └─┘                        └─
st   ───────────────────────────────────────────────────────────────
534      ... = _ :
src  ───────┘ └────
typ  ───────┘ └────
doc  ───────┘ └────
txt  ───────┘ └────
par  ───────┘ └────
pid  ───────┘ └────
st   ──────────────
535      begin
src  ───┘     
typ  ───┘     
doc  ───┘     
txt  ───┘     
par  ───┘     
pid  ───┘     
st   ───┘└─────
536        convert rfl,
id                 └─┘
src  ─────┘└──────┘└─┘└─
typ  ─────┘└──────┘└─┘└─
doc  ─────┘└──────┘   └─
txt  ─────┘└──────┘   └─
par  ─────┘└──────┘   └─
pid  ─────────────┘   └─
st   ────────────────┘└─
537        { rw ← coe_nnnorm, rw [ennreal.of_real], congr, exact nnreal.of_real_coe },
id                └────────┘      └─────────────┘                └────────────────┘
src  ───────┘└───┘└────────┘└┘└──┘└─────────────┘└┘└───┘└──────┘└────────────────┘└───
typ  ───────┘└───┘└────────┘└┘└──┘└─────────────┘└┘└───┘└──────┘└────────────────┘└───
doc  ───────┘└───┘          └┘└──┘└─────────────┘└┘     └──────┘                  └───
txt  ───────┘└───┘          └┘└──┘               └┘└───┘└──────┘                  └───
par  ───────┘└───┘          └┘└──┘               └┘└───┘└──────┘                  └───
pid  ────────────┘          └────┘               └──────────────┘                  └───
st   ──────┘└──────────────┘└───────────────────┘└──────┘└─────────────────────────┘└─
538        { funext, simp [nndist_eq_nnnorm] }
id                         └──────────────┘
src  ───────┘└────┘└┘└────┘└──────────────┘└┘└─
typ  ───────┘└────┘└┘└────┘└──────────────┘└┘└─
doc  ───────┘└────┘└┘└────┘                └┘└─
txt  ───────┘└────┘└┘└────┘                └┘└─
par  ───────┘└────┘└┘└────┘                └┘└─
pid  ─────────────────────┘                └───
st   ─────────────┘└────────────────────────┘└─
539      end,
src  ──────┘
typ  ──────┘
doc  ──────┘
txt  ──────┘
par  ──────┘
pid  ──────┘
st   ─────────
540  end
st   ──┘
541  
542  end normed_space
543  
544  section pos_part
545  
546  variables {γ : Type*} [topological_space γ] [decidable_linear_order γ] [order_closed_topology γ]
id                          └───────────────┘     └────────────────────┘     └───────────────────┘
src                         └───────────────┘     └────────────────────┘     └───────────────────┘
typ                         └───────────────┘     └────────────────────┘     └───────────────────┘
doc                         └───────────────┘                                └───────────────────┘
547    [second_countable_topology γ] [has_zero γ]
id      └───────────────────────┘     └──────┘
src     └───────────────────────┘     └──────┘
typ     └───────────────────────┘     └──────┘
doc     └───────────────────────┘
548  
549  /-- Positive part of an `ae_eq_fun`. -/
550  def pos_part (f : α →ₘ γ) : α →ₘ γ :=
id                      └┘      └┘ 
src                      └┘        └┘
typ                     └┘      └┘ 
doc                      └┘        └┘
551  comp₂ max (measurable.max (measurable.fst measurable_id) (measurable.snd measurable_id)) f 0
id   └───┘ └─┘  └────────────┘  └────────────┘ └───────────┘   └────────────┘ └───────────┘   
src  └───┘ └─┘  └────────────┘  └────────────┘ └───────────┘   └────────────┘ └───────────┘
typ  └───┘ └─┘  └────────────┘  └────────────┘ └───────────┘   └────────────┘ └───────────┘   
doc  └───┘
552  
553  lemma pos_part_to_fun (f : α →ₘ γ) : ∀ₘ a, (pos_part f).to_fun a = max (f.to_fun a) (0:γ) :=
id                               └┘     └┘   └──────┘  └────┘    └─┘  └─────┘      
src                               └┘      └┘    └──────┘   └────┘     └─┘   └─────┘
typ                              └┘     └┘   └──────┘  └────┘    └─┘  └─────┘      
doc                               └┘      └┘    └──────┘   └────┘            └─────┘
554  begin
st   └─────
555    filter_upwards [comp₂_to_fun max (measurable.max (measurable.fst measurable_id)
id                     └──────────┘ └─┘  └────────────┘  └────────────┘
src    └──────────────┘└──────────┘└─┘ └────────────┘ └────────────┘             └─
typ    └──────────────┘└──────────┘└─┘ └────────────┘ └────────────┘             └─
doc    └──────────────┘                                                          └─
txt    └──────────────┘                                                          └─
par    └──────────────┘                                                          └─
pid                  └┘                                                          └─
st   ──────────────────────────────────────────────────────────────────────────────────
556      (measurable.snd measurable_id)) f 0, @ae_eq_fun.zero_to_fun α γ],
id        └────────────┘ └───────────┘        └───────────────────┘  
src  ───┘ └────────────┘└───────────┘└─┘ └──┘ └───────────────────┘  
typ  ───┘ └────────────┘└───────────┘└─┘└──┘ └───────────────────┘
doc  ───┘                            └─┘ └──┘                        
txt  ───┘                            └─┘ └──┘                        
par  ───┘                            └─┘ └──┘                        
pid  ───┘                            └─┘ └──┘                        
st   ───────────────────────────────────────────────────────────────────┘└─
557    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
558    assume a h₁ h₂,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid    └────────────┘
st   ───────────────┘└─
559    rw [pos_part, h₁, h₂]
id         └──────┘  └┘  └┘
src    └──┘└──────┘└┘  └┘  └┘
typ    └──┘└──────┘└┘└┘└┘└┘└┘
doc    └──┘└──────┘└┘  └┘  └┘
txt    └──┘        └┘  └┘  └┘
par    └──┘        └┘  └┘  └┘
pid      └┘        └┘  └┘  
st   ─────────────┘└──┘└──┘
560  end
st   └─┘
561  
562  end pos_part
563  
564  end ae_eq_fun
565  
566  end measure_theory